\begin{tabbing}
$\forall$\=${\it es}$:ES, $P_{1}$, $P_{2}$:(E$\rightarrow\mathbb{P}$), $Q_{1}$, $R_{1}$, $Q_{2}$, $R_{2}$:(E$\rightarrow$E$\rightarrow\mathbb{P}$), ${\it dcd\_P}_{1}$:($e$:E$\rightarrow$Dec($P_{1}$($e$))),\+
\\[0ex]$f_{1}$:(\{$e$:E$\mid$ $P_{1}$($e$)\} $\rightarrow$E), $f_{2}$:(\{$e$:E$\mid$ $P_{2}$($e$)\} $\rightarrow$E).
\-\\[0ex]($\forall$$e$, ${\it e'}$:\{$e$:E$\mid$ $P_{1}$($e$)\} . $\neg$($Q_{2}$($f_{1}$($e$),$f_{1}$(${\it e'}$))))
\\[0ex]$\Rightarrow$ ($\forall$$e$, ${\it e'}$:\{$e$:E$\mid$ $P_{2}$($e$)\} . $\neg$($Q_{1}$($f_{2}$($e$),$f_{2}$(${\it e'}$))))
\\[0ex]$\Rightarrow$ \=($\forall$$e$:\{$e$:E$\mid$ $P_{1}$($e$)\} , ${\it e'}$:\{$e$:E$\mid$ $P_{2}$($e$)\} .\+
\\[0ex]($\neg$($Q_{1}$($f_{1}$($e$),$f_{2}$(${\it e'}$))))
\\[0ex]\& ($\neg$($Q_{1}$($f_{2}$(${\it e'}$),$f_{1}$($e$))))
\\[0ex]\& ($\neg$($Q_{2}$($f_{1}$($e$),$f_{2}$(${\it e'}$))))
\\[0ex]\& ($\neg$($Q_{2}$($f_{2}$(${\it e'}$),$f_{1}$($e$)))))
\-\\[0ex]$\Rightarrow$ $f_{1}$ is $Q_{1}${-}$R_{1}${-}pre{-}preserving on $P_{1}$
\\[0ex]$\Rightarrow$ $f_{2}$ is $Q_{2}${-}$R_{2}${-}pre{-}preserving on $P_{2}$
\\[0ex]$\Rightarrow$ [$P_{1}$? $f_{1}$ : $f_{2}$] is $Q_{1}$ $\vee$ $Q_{2}${-}$R_{1}$ $\vee$ $R_{2}${-}pre{-}preserving on $P_{1}$ $\vee$ $P_{2}$
\end{tabbing}